SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Cook–Levin theorem</title>

</head>

Cook–Levin theorem

</h1>

</header>

In <a href="Computational_complexity_theory" title="Computational complexity theory">computational complexity theory</a>, the Cook–Levin theorem, also known as Cook's theorem, states that the <a href="Boolean_satisfiability_problem" title="Boolean satisfiability problem">Boolean satisfiability problem</a> is <a href="NP-completeness" title="NP-completeness">NP-complete</a>. That is, it is in <a href="NP_(complexity)" title="NP (complexity)">NP</a>, and any problem in NP can be <a href="Reduction_(complexity)" title="Reduction (complexity)">reduced</a> in <a href="Polynomial_time" class="mw-redirect" title="Polynomial time">polynomial time</a> by a <a href="Deterministic_Turing_machine" class="mw-redirect" title="Deterministic Turing machine">deterministic Turing machine</a> to the Boolean satisfiability problem.

The theorem is named after <a href="Stephen_Cook" title="Stephen Cook">Stephen Cook</a> and <a href="Leonid_Levin" title="Leonid Levin">Leonid Levin</a>. The proof is due to <a href="Richard_Karp" class="mw-redirect" title="Richard Karp">Richard Karp</a>, based on an earlier proof (using a different notion of reducibility) by Cook.<a href="#cite_note-Karp-1">[1]</a>

An important consequence of this theorem is that if there exists a deterministic polynomial-time algorithm for solving Boolean satisfiability, then every <a href="NP_(complexity)" title="NP (complexity)">NP</a> problem can be solved by a deterministic polynomial-time algorithm. The question of whether such an algorithm for Boolean satisfiability exists is thus equivalent to the <a href="P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a>, which is still widely considered the most important unsolved problem in <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a>.

<div class="mw-heading mw-heading2"><h2 id="Contributions">Contributions</h2></div>

The concept of <a href="NP-completeness" title="NP-completeness">NP-completeness</a> was developed in the late 1960s and early 1970s in parallel by researchers in North America and the <a href="Soviet_Union" title="Soviet Union">Soviet Union</a>.

In 1971, <a href="Stephen_Cook" title="Stephen Cook">Stephen Cook</a> published his paper "The complexity of theorem proving procedures"<a href="#cite_note-2">[2]</a> in conference proceedings of the newly founded ACM <a href="Symposium_on_Theory_of_Computing" title="Symposium on Theory of Computing">Symposium on Theory of Computing</a>. <a href="Richard_Karp" class="mw-redirect" title="Richard Karp">Richard Karp</a>'s subsequent paper, "Reducibility among

combinatorial problems",<a href="#cite_note-Karp-1">[1]</a> generated renewed interest in Cook's paper by providing a <a href="Karp's_21_NP-complete_problems" title="Karp's 21 NP-complete problems">list of 21 NP-complete problems</a>. Karp also introduced the notion of completeness used in the current definition of NP-completeness (i.e., by <a href="Polynomial-time_many-one_reduction" class="mw-redirect" title="Polynomial-time many-one reduction">polynomial-time many-one reduction</a>). Cook and Karp each received a <a href="Turing_Award" title="Turing Award">Turing Award</a> for this work.

The theoretical interest in NP-completeness was also enhanced by the work of Theodore P. Baker, John Gill, and <a href="Robert_Solovay" class="mw-redirect" title="Robert Solovay">Robert Solovay</a> who showed, in 1975, that solving NP-problems in certain <a href="Oracle_machine" title="Oracle machine">oracle machine</a> models requires exponential time. That is, there exists an oracle A such that, for all subexponential deterministic-time complexity classes T, the relativized complexity class NPA is not a subset of TA. In particular, for this oracle, PA ≠ NPA.<a href="#cite_note-3">[3]</a>

In the USSR, a result equivalent to Baker, Gill, and Solovay's was published in 1969 by M. Dekhtiar.<a href="#cite_note-4">[4]</a> Later <a href="Leonid_Levin" title="Leonid Levin">Leonid Levin</a>'s paper, "Universal search problems",<a href="#cite_note-5">[5]</a> was published in 1973, although it was mentioned in talks and submitted for publication a few years earlier.

Levin's approach was slightly different from Cook's and Karp's in that he considered <a href="Search_problem" title="Search problem">search problems</a>, which require finding solutions rather than simply determining existence. He provided six such NP-complete search problems, or universal problems.

Additionally he found for each of these problems an algorithm that solves it in optimal time (in particular, these algorithms run in polynomial time if and only if <a href="P_versus_NP_problem" title="P versus NP problem">P = NP</a>).

<div class="mw-heading mw-heading2"><h2 id="Definitions">Definitions</h2></div>

A <a href="Decision_problem" title="Decision problem">decision problem</a> is in <a href="NP_(complexity)" title="NP (complexity)">NP</a> if it can be decided by a <a href="Nondeterministic_Turing_machine" title="Nondeterministic Turing machine">nondeterministic Turing machine</a> in <a href="Polynomial_time" class="mw-redirect" title="Polynomial time">polynomial time</a>.

An instance of the Boolean satisfiability problem is a <a href="Boolean_expression" title="Boolean expression">Boolean expression</a> that combines <a href="Boolean_variable" class="mw-redirect" title="Boolean variable">Boolean variables</a> using <a href="Logical_connective" title="Logical connective">Boolean operators</a>.

Such an expression is satisfiable if there is some assignment of <a href="Truth_value" title="Truth value">truth values</a> to the variables that makes the entire expression true.

Given any decision problem in NP, construct a non-deterministic machine that solves it in polynomial time. Then for each input to that machine, build a Boolean expression that computes whether when that specific input is passed to the machine, the machine runs correctly, and the machine halts and answers "yes". Then the expression can be satisfied if and only if there is a way for the machine to run correctly and answer "yes", so the satisfiability of the constructed expression is equivalent to asking whether or not the machine will answer "yes".

<div class="mw-heading mw-heading2"><h2 id="Proof">Proof</h2></div>

This proof is based on the one given by <a href="#CITEREFGareyJohnson1979">Garey & Johnson 1979</a>, pp. 38–44, Section 2.6.

There are two parts to proving that the Boolean satisfiability problem (SAT) is NP-complete. One is to show that SAT is an NP problem. The other is to show that every NP problem can be reduced to an instance of a SAT problem by a <a href="Polynomial-time_many-one_reduction" class="mw-redirect" title="Polynomial-time many-one reduction">polynomial-time many-one reduction</a>.

SAT is in NP because any assignment of Boolean values to Boolean variables that is claimed to satisfy the given expression can be verified in polynomial time by a deterministic Turing machine. (The statements verifiable in polynomial time by a deterministic Turing machine and solvable in polynomial time by a non-deterministic Turing machine are equivalent, and the proof can be found in many textbooks, for example Sipser's Introduction to the Theory of Computation, section 7.3., as well as <a href="NP_(complexity)#Equivalence_of_definitions" title="NP (complexity)">in the Wikipedia article on NP</a>).

Now suppose that a given problem in NP can be solved by the <a href="Nondeterministic_Turing_machine" title="Nondeterministic Turing machine">nondeterministic Turing machine</a> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M=(Q,\Sigma ,s,F,\delta )}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M=(Q,\Sigma ,s,F,\delta )}</annotation>

</semantics>

</math><img src="./4b17ffda902834ec267975d809b7206eeece547f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.882ex; height:2.843ex;" alt="{\displaystyle M=(Q,\Sigma ,s,F,\delta )}" loading="lazy">, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q}</annotation>

</semantics>

</math><img src="./8752c7023b4b3286800fe3238271bbca681219ed.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}" loading="lazy"> is the set of states, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>

</semantics>

</math><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"> is the alphabet of tape symbols, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle s\in Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle s\in Q}</annotation>

</semantics>

</math><img src="./baa662d061d25282ee121464d38bc961522e7219.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.769ex; height:2.509ex;" alt="{\displaystyle s\in Q}" loading="lazy"> is the initial state, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F\subseteq Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F\subseteq Q}</annotation>

</semantics>

</math><img src="./9ada8f098adcf02f7a674d2a5f2dda5e4917881e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.678ex; height:2.509ex;" alt="{\displaystyle F\subseteq Q}" loading="lazy"> is the set of accepting states, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \delta \subseteq ((Q\setminus F)\times \Sigma )\times (Q\times \Sigma \times \{-1,+1\})}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \delta \subseteq ((Q\setminus F)\times \Sigma )\times (Q\times \Sigma \times \{-1,+1\})}</annotation>

</semantics>

</math><img src="./ca52d5c2e26b01ab66e56b2ca556bcd949cd516a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:41.205ex; height:2.843ex;" alt="{\displaystyle \delta \subseteq ((Q\setminus F)\times \Sigma )\times (Q\times \Sigma \times \{-1,+1\})}" loading="lazy"> is the transition relation. Suppose further that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy"> accepts or rejects an instance of the problem after at most <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p(n)}</annotation>

</semantics>

</math><img src="./0e7d5ae3aa9524f57fb8b44ac46ee8cf6a52d7e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:4.463ex; height:2.843ex;" alt="{\displaystyle p(n)}" loading="lazy"> computation steps, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy"> is the size of the instance and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"> is a polynomial function.

For each input, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle I}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle I}</annotation>

</semantics>

</math><img src="./535ea7fc4134a31cbe2251d9d3511374bc41be9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.172ex; height:2.176ex;" alt="{\displaystyle I}" loading="lazy">, specify a Boolean expression <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle B}</annotation>

</semantics>

</math><img src="./47136aad860d145f75f3eed3022df827cee94d7a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}" loading="lazy"> that is satisfiable <a href="If_and_only_if" title="If and only if">if and only if</a> the machine <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy"> accepts <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle I}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle I}</annotation>

</semantics>

</math><img src="./535ea7fc4134a31cbe2251d9d3511374bc41be9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.172ex; height:2.176ex;" alt="{\displaystyle I}" loading="lazy">.

The Boolean expression uses the variables set out in the following table. Here, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q\in Q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q\in Q}</annotation>

</semantics>

</math><img src="./960b889a6324eeccc02725962bf11ac1a96c32fd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.749ex; height:2.509ex;" alt="{\displaystyle q\in Q}" loading="lazy"> is a machine state, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle -p(n)\leq i\leq p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle -p(n)\leq i\leq p(n)}</annotation>

</semantics>

</math><img src="./a59e57d1b7189e6c26116f5ba31ee76385120ecf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.554ex; height:2.843ex;" alt="{\displaystyle -p(n)\leq i\leq p(n)}" loading="lazy"> is a tape position, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle j\in \Sigma }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j\in \Sigma }</annotation>

</semantics>

</math><img src="./2dc342e411cd3ab923cb2cde647f23e2eaf3d54f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.027ex; width:5.504ex; height:2.509ex;" alt="{\displaystyle j\in \Sigma }" loading="lazy"> is a tape symbol, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0\leq k\leq p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 0\leq k\leq p(n)}</annotation>

</semantics>

</math><img src="./4c33bcb7d0b7f9517dc5f06387760914eef7858e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.944ex; height:2.843ex;" alt="{\displaystyle 0\leq k\leq p(n)}" loading="lazy"> is the number of a computation step.

<th>Variables

</th>

<th>Intended interpretation

</th>

</th></tr>

<tr>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{i,j,k}}</annotation>

</semantics>

</math><img src="./c137df3c98c7b5c7f3b2b3622d75f468c114009f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.606ex; height:2.843ex;" alt="{\displaystyle T_{i,j,k}}" loading="lazy">

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy"> contains symbol <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle j}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j}</annotation>

</semantics>

</math><img src="./2f461e54f5c093e92a55547b9764291390f0b5d0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.027ex; width:0.985ex; height:2.509ex;" alt="{\displaystyle j}" loading="lazy"> at step <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k}</annotation>

</semantics>

</math><img src="./c3c9a2c7b599b37105512c5d570edc034056dd40.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.211ex; height:2.176ex;" alt="{\displaystyle k}" loading="lazy"> of the computation.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy">

</td></tr>

<tr>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle H_{i,k}}</annotation>

</semantics>

</math><img src="./feea1bfc2b80ba25f51d11b20bbef5287bda034f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.045ex; height:2.843ex;" alt="{\displaystyle H_{i,k}}" loading="lazy">

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy">'s read/write head is at tape cell <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy"> at step <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k}</annotation>

</semantics>

</math><img src="./c3c9a2c7b599b37105512c5d570edc034056dd40.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.211ex; height:2.176ex;" alt="{\displaystyle k}" loading="lazy"> of the computation.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy">

</td></tr>

<tr>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q_{q,k}}</annotation>

</semantics>

</math><img src="./4f199504f66dd77a330fd27f0319926b1687fab6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.141ex; height:2.843ex;" alt="{\displaystyle Q_{q,k}}" loading="lazy">

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy"> is in state <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy"> at step <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k}</annotation>

</semantics>

</math><img src="./c3c9a2c7b599b37105512c5d570edc034056dd40.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.211ex; height:2.176ex;" alt="{\displaystyle k}" loading="lazy"> of the computation.

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n))}</annotation>

</semantics>

</math><img src="./a6282d62acd69fcf285bd848594f4daafd2b4a3e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.956ex; height:2.843ex;" alt="{\displaystyle O(p(n))}" loading="lazy">

</td></tr></tbody></table>

Define the Boolean expression <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle B}</annotation>

</semantics>

</math><img src="./47136aad860d145f75f3eed3022df827cee94d7a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}" loading="lazy"> to be the <a href="Logical_conjunction" title="Logical conjunction">conjunction</a> of the sub-expressions in the following table, for all <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle -p(n)\leq i\leq p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle -p(n)\leq i\leq p(n)}</annotation>

</semantics>

</math><img src="./a59e57d1b7189e6c26116f5ba31ee76385120ecf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.554ex; height:2.843ex;" alt="{\displaystyle -p(n)\leq i\leq p(n)}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0\leq k\leq p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 0\leq k\leq p(n)}</annotation>

</semantics>

</math><img src="./4c33bcb7d0b7f9517dc5f06387760914eef7858e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.944ex; height:2.843ex;" alt="{\displaystyle 0\leq k\leq p(n)}" loading="lazy">:

<th>Expression

</th>

<th>Conditions

</th>

<th>Interpretation

</th>

<th>How many?

</th></tr>

<tr>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{i,j,0}}</annotation>

</semantics>

</math><img src="./29181927730e6a6bc1eecb835178e49a8448d238.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.571ex; height:2.843ex;" alt="{\displaystyle T_{i,j,0}}" loading="lazy">

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy"> initially contains symbol <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle j}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j}</annotation>

</semantics>

</math><img src="./2f461e54f5c093e92a55547b9764291390f0b5d0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.027ex; width:0.985ex; height:2.509ex;" alt="{\displaystyle j}" loading="lazy">

</td>

<td>Initial contents of the tape. For <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i>n-1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i>n-1}</annotation>

</semantics>

</math><img src="./849f077bfda03a6182f6edcfebe72afb82abf76c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:9.298ex; height:2.343ex;" alt="{\displaystyle i>n-1}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i<0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i<0}</annotation>

</semantics>

</math><img src="./2211a8fa50853fffd51a8da66b8f0881522e7e80.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.063ex; height:2.176ex;" alt="{\displaystyle i<0}" loading="lazy">, outside of the actual input <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle I}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle I}</annotation>

</semantics>

</math><img src="./535ea7fc4134a31cbe2251d9d3511374bc41be9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.172ex; height:2.176ex;" alt="{\displaystyle I}" loading="lazy">, the initial symbol is the special default/blank symbol.

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n))}</annotation>

</semantics>

</math><img src="./a6282d62acd69fcf285bd848594f4daafd2b4a3e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.956ex; height:2.843ex;" alt="{\displaystyle O(p(n))}" loading="lazy">

</td></tr>

<tr>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q_{s,0}}</annotation>

</semantics>

</math><img src="./a61e8a2b009588140dc0fc85545369d577e8719b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.121ex; height:2.843ex;" alt="{\displaystyle Q_{s,0}}" loading="lazy">

</td>

<td>

</td>

<td>Initial state of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy">.

</td>

<td>1

</td></tr>

<tr>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle H_{0,0}}</annotation>

</semantics>

</math><img src="./3655904fa5f242794e700f4f0cbfea5f049f2d65.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.265ex; height:2.843ex;" alt="{\displaystyle H_{0,0}}" loading="lazy">

</td>

<td>

</td>

<td>Initial position of read/write head.

</td>

<td>1

</td></tr>

<tr>

<msub>

</mrow>

</msub>

<msub>

<msup>

</msup>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg T_{i,j,k}\lor \neg T_{i,j',k}}</annotation>

</semantics>

</math><img src="./4f70c47d831e3035dc655e18bb9dd52ec0945e82.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.171ex; width:15.427ex; height:3.009ex;" alt="{\displaystyle \neg T_{i,j,k}\lor \neg T_{i,j',k}}" loading="lazy">

</td>

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j\neq j'}</annotation>

</semantics>

</math><img src="./12ed85137b914f204fb3833f913d1de3f520a981.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.027ex; width:5.726ex; height:3.009ex;" alt="{\displaystyle j\neq j'}" loading="lazy">

</td>

<td>At most one symbol per tape cell.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy">

</td></tr>

<tr>

</mrow>

</munder>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bigvee _{j\in \Sigma }T_{i,j,k}}</annotation>

</semantics>

</math><img src="./20fc7ab5cf64313d8256f5b20c1302cfb451d436.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.338ex; margin-left: -0.019ex; width:7.972ex; height:5.843ex;" alt="{\displaystyle \bigvee _{j\in \Sigma }T_{i,j,k}}" loading="lazy">

</td>

<td>

</td>

<td>At least one symbol per tape cell.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy">

</td></tr>

<tr>

<msub>

</mrow>

</msub>

<msub>

<msup>

</msup>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{i,j,k}\land T_{i,j',k+1}\rightarrow H_{i,k}}</annotation>

</semantics>

</math><img src="./a5955b1d9dc20e5d50807ece03da97498eed907c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.171ex; width:22.085ex; height:3.009ex;" alt="{\displaystyle T_{i,j,k}\land T_{i,j',k+1}\rightarrow H_{i,k}}" loading="lazy">

</td>

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j\neq j'}</annotation>

</semantics>

</math><img src="./12ed85137b914f204fb3833f913d1de3f520a981.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.027ex; width:5.726ex; height:3.009ex;" alt="{\displaystyle j\neq j'}" loading="lazy">

</td>

<td>Tape remains unchanged unless written by head.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy">

</td></tr>

<tr>

<msub>

</mrow>

</msub>

<msub>

<msup>

</msup>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lnot Q_{q,k}\lor \lnot Q_{q',k}}</annotation>

</semantics>

</math><img src="./107158f1d1a4c3ff0832319414368237b24bd623.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:14.503ex; height:2.843ex;" alt="{\displaystyle \lnot Q_{q,k}\lor \lnot Q_{q',k}}" loading="lazy">

</td>

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q\neq q'}</annotation>

</semantics>

</math><img src="./33b1ca878f514e30c6ae11b5dced419d004c5062.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.932ex; height:3.009ex;" alt="{\displaystyle q\neq q'}" loading="lazy">

</td>

<td>At most one state at a time.

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n))}</annotation>

</semantics>

</math><img src="./a6282d62acd69fcf285bd848594f4daafd2b4a3e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.956ex; height:2.843ex;" alt="{\displaystyle O(p(n))}" loading="lazy">

</td></tr>

<tr>

</mrow>

</munder>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bigvee _{q\in Q}Q_{q,k}}</annotation>

</semantics>

</math><img src="./16dd65b442cc1d003930603ebdb20e22f91cb60d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.338ex; width:7.68ex; height:5.843ex;" alt="{\displaystyle \bigvee _{q\in Q}Q_{q,k}}" loading="lazy">

</td>

<td>

</td>

<td>At least one state at a time.

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n))}</annotation>

</semantics>

</math><img src="./a6282d62acd69fcf285bd848594f4daafd2b4a3e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.956ex; height:2.843ex;" alt="{\displaystyle O(p(n))}" loading="lazy">

</td></tr>

<tr>

<msub>

</mrow>

</msub>

<msub>

<msup>

</msup>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lnot H_{i,k}\lor \lnot H_{i',k}}</annotation>

</semantics>

</math><img src="./df5eb255ef0bfe81be0f8fbf558b2e87c8da047c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.171ex; width:14.304ex; height:3.009ex;" alt="{\displaystyle \lnot H_{i,k}\lor \lnot H_{i',k}}" loading="lazy">

</td>

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i\neq i'}</annotation>

</semantics>

</math><img src="./900d862e3d76b2767561f155e0aeb14fe6ad25e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.388ex; height:3.009ex;" alt="{\displaystyle i\neq i'}" loading="lazy">

</td>

<td>At most one head position at a time.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{3})}</annotation>

</semantics>

</math><img src="./32bdb093a5eb1380b038597f38fccbde571d3663.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{3})}" loading="lazy">

</td></tr>

<tr>

</mrow>

</munder>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bigvee _{-p(n)\leq i\leq p(n)}H_{i,k}}</annotation>

</semantics>

</math><img src="./85e9a1fd79e3cb5a6149e02e323bf11cdd507f2c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.505ex; width:15.02ex; height:6.009ex;" alt="{\displaystyle \bigvee _{-p(n)\leq i\leq p(n)}H_{i,k}}" loading="lazy">

</td>

<td>

</td>

<td>At least one head position at a time.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy">

</td></tr>

<tr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msup>

</msup>

<msup>

</msup>

</mrow>

</munder>

<msub>

</mrow>

</msub>

<msub>

<msup>

</msup>

</mrow>

</msub>

<msub>

<msup>

</msup>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{l}(H_{i,k}\land Q_{q,k}\land T_{i,\sigma ,k})\to \\\bigvee _{((q,\sigma ),(q',\sigma ',d))\in \delta }(H_{i+d,\ k+1}\land Q_{q',\ k+1}\land T_{i,\ \sigma ',\ k+1})\end{array}}}</annotation>

</semantics>

</math><img src="./3b6a3bd9679d38c63b9851bb0d1a545295f2b9bb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.838ex; width:47.61ex; height:6.843ex;" alt="{\displaystyle {\begin{array}{l}(H_{i,k}\land Q_{q,k}\land T_{i,\sigma ,k})\to \\\bigvee _{((q,\sigma ),(q',\sigma ',d))\in \delta }(H_{i+d,\ k+1}\land Q_{q',\ k+1}\land T_{i,\ \sigma ',\ k+1})\end{array}}}" loading="lazy">

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k<p(n)}</annotation>

</semantics>

</math><img src="./575cbf9a0fdb85a22d9eaaa4716285e70054cd4e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.683ex; height:2.843ex;" alt="{\displaystyle k<p(n)}" loading="lazy">

</td>

<td>Possible transitions at computation step <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k}</annotation>

</semantics>

</math><img src="./c3c9a2c7b599b37105512c5d570edc034056dd40.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.211ex; height:2.176ex;" alt="{\displaystyle k}" loading="lazy"> when head is at position <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy">.

</td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy">

</td></tr>

<tr>

</mrow>

</munder>

</mrow>

</munder>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bigvee _{0\leq k\leq p(n)}\bigvee _{f\in F}Q_{f,k}}</annotation>

</semantics>

</math><img src="./35345590c7e7f31fb7f9690b055f6ed1e831139f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.505ex; width:15.622ex; height:6.009ex;" alt="{\displaystyle \bigvee _{0\leq k\leq p(n)}\bigvee _{f\in F}Q_{f,k}}" loading="lazy">

</td>

<td>

</td>

<td>Must finish in an accepting state, not later than in step <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p(n)}</annotation>

</semantics>

</math><img src="./0e7d5ae3aa9524f57fb8b44ac46ee8cf6a52d7e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:4.463ex; height:2.843ex;" alt="{\displaystyle p(n)}" loading="lazy">.

</td>

<td>1

</td></tr></tbody></table>

If there is an accepting computation for <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy"> on input <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle I}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle I}</annotation>

</semantics>

</math><img src="./535ea7fc4134a31cbe2251d9d3511374bc41be9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.172ex; height:2.176ex;" alt="{\displaystyle I}" loading="lazy">, then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle B}</annotation>

</semantics>

</math><img src="./47136aad860d145f75f3eed3022df827cee94d7a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}" loading="lazy"> is satisfiable by assigning <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{i,j,k}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{i,j,k}}</annotation>

</semantics>

</math><img src="./c137df3c98c7b5c7f3b2b3622d75f468c114009f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.606ex; height:2.843ex;" alt="{\displaystyle T_{i,j,k}}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle H_{i,k}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle H_{i,k}}</annotation>

</semantics>

</math><img src="./feea1bfc2b80ba25f51d11b20bbef5287bda034f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.045ex; height:2.843ex;" alt="{\displaystyle H_{i,k}}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Q_{i,k}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Q_{i,k}}</annotation>

</semantics>

</math><img src="./e077beb8a941fa3f120a46d01b0efa18c115d220.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:3.952ex; height:2.843ex;" alt="{\displaystyle Q_{i,k}}" loading="lazy"> their intended interpretations. On the other hand, if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle B}</annotation>

</semantics>

</math><img src="./47136aad860d145f75f3eed3022df827cee94d7a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}" loading="lazy"> is satisfiable, then there is an accepting computation for <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy"> on input <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle I}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle I}</annotation>

</semantics>

</math><img src="./535ea7fc4134a31cbe2251d9d3511374bc41be9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.172ex; height:2.176ex;" alt="{\displaystyle I}" loading="lazy"> that follows the steps indicated by the assignments to the variables.

There are <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(p(n)^{2})}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{2})}</annotation>

</semantics>

</math><img src="./3f901a28545c890bba2ed7bbe3183325fe377b12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{2})}" loading="lazy"> Boolean variables, each encodable in space <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(\log p(n))}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(\log p(n))}</annotation>

</semantics>

</math><img src="./b88599f2803db7b737c2bacf4430e528d7d4f8ba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.315ex; height:2.843ex;" alt="{\displaystyle O(\log p(n))}" loading="lazy">. The number of clauses is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(p(n)^{3})}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)^{3})}</annotation>

</semantics>

</math><img src="./32bdb093a5eb1380b038597f38fccbde571d3663.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.01ex; height:3.176ex;" alt="{\displaystyle O(p(n)^{3})}" loading="lazy"><a href="#cite_note-7">[7]</a> so the size of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle B}</annotation>

</semantics>

</math><img src="./47136aad860d145f75f3eed3022df827cee94d7a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}" loading="lazy"> is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(\log(p(n))p(n)^{3})}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(\log(p(n))p(n)^{3})}</annotation>

</semantics>

</math><img src="./fc8fa42ac4d414a9f72fc71fd7ae0226efcf0756.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.165ex; height:3.176ex;" alt="{\displaystyle O(\log(p(n))p(n)^{3})}" loading="lazy">. Thus the transformation is certainly a polynomial-time many-one reduction, as required.

Only the first table row (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{i,j,0}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{i,j,0}}</annotation>

</semantics>

</math><img src="./29181927730e6a6bc1eecb835178e49a8448d238.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.571ex; height:2.843ex;" alt="{\displaystyle T_{i,j,0}}" loading="lazy">) actually depends on the input string <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle I}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle I}</annotation>

</semantics>

</math><img src="./535ea7fc4134a31cbe2251d9d3511374bc41be9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.172ex; height:2.176ex;" alt="{\displaystyle I}" loading="lazy">. The remaining lines depend only on the input length <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy"> and on the machine <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy">; they formalize a generic computation of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy"> for up to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p(n)}</annotation>

</semantics>

</math><img src="./0e7d5ae3aa9524f57fb8b44ac46ee8cf6a52d7e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:4.463ex; height:2.843ex;" alt="{\displaystyle p(n)}" loading="lazy"> steps.

The transformation makes extensive use of the polynomial <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p(n)}</annotation>

</semantics>

</math><img src="./0e7d5ae3aa9524f57fb8b44ac46ee8cf6a52d7e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:4.463ex; height:2.843ex;" alt="{\displaystyle p(n)}" loading="lazy">. As a consequence, the above proof is not <a href="Constructive_proof" title="Constructive proof">constructive</a>: even if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy"> is known, <a href="Witness_(mathematics)" title="Witness (mathematics)">witnessing</a> the membership of the given problem in NP, the transformation cannot be effectively computed, unless an upper bound <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p(n)}</annotation>

</semantics>

</math><img src="./0e7d5ae3aa9524f57fb8b44ac46ee8cf6a52d7e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:4.463ex; height:2.843ex;" alt="{\displaystyle p(n)}" loading="lazy"> of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M}</annotation>

</semantics>

</math><img src="./f82cade9898ced02fdd08712e5f0c0151758a0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}" loading="lazy">'s time complexity is also known.

<div class="mw-heading mw-heading2"><h2 id="Complexity">Complexity</h2></div>

While the above method encodes a non-deterministic Turing machine in complexity <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(\log(p(n))p(n)^{3})}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(\log(p(n))p(n)^{3})}</annotation>

</semantics>

</math><img src="./fc8fa42ac4d414a9f72fc71fd7ae0226efcf0756.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.165ex; height:3.176ex;" alt="{\displaystyle O(\log(p(n))p(n)^{3})}" loading="lazy">, the literature describes more sophisticated approaches in complexity <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(p(n)\log(p(n)))}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n)\log(p(n)))}</annotation>

</semantics>

</math><img src="./0d85954d751285ff6ea58aace75d5387f6ead4b6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.498ex; height:2.843ex;" alt="{\displaystyle O(p(n)\log(p(n)))}" loading="lazy">.<a href="#cite_note-8">[8]</a><a href="#cite_note-9">[9]</a><a href="#cite_note-10">[10]</a><a href="#cite_note-11">[11]</a><a href="#cite_note-12">[12]</a> The quasilinear result first appeared seven years after Cook's original publication.

The use of SAT to prove the existence of an NP-complete problem can be extended to other computational problems in logic, and to completeness for other <a href="Complexity_class" title="Complexity class">complexity classes</a>.

The <a href="Quantified_Boolean_formula" class="mw-redirect" title="Quantified Boolean formula">quantified Boolean formula</a> problem (QBF) involves Boolean formulas extended to include nested <a href="Universal_quantifier" class="mw-redirect" title="Universal quantifier">universal quantifiers</a> and <a href="Existential_quantifier" class="mw-redirect" title="Existential quantifier">existential quantifiers</a> for its variables. The QBF problem can be used to encode computation with a Turing machine limited to <a href="PSPACE" title="PSPACE">polynomial space complexity</a>, proving that there exists a problem (the recognition of true quantified Boolean formulas) that is <a href="PSPACE-complete" title="PSPACE-complete">PSPACE-complete</a>. Analogously, dependency quantified boolean formulas encode computation with a Turing machine limited to <a href="NL_(complexity)" title="NL (complexity)">logarithmic space complexity</a>, proving that there exists a problem that is <a href="NL-complete" title="NL-complete">NL-complete</a>.<a href="#cite_note-13">[13]</a><a href="#cite_note-14">[14]</a>

<div class="mw-heading mw-heading2"><h2 id="Consequences">Consequences</h2></div>

The proof shows that every problem in NP can be reduced in polynomial time (in fact, <a href="Logarithmic_space" class="mw-redirect" title="Logarithmic space">logarithmic space</a> suffices) to an instance of the Boolean satisfiability problem. This means that if the Boolean satisfiability problem could be solved in polynomial time by a <a href="Deterministic_Turing_machine" class="mw-redirect" title="Deterministic Turing machine">deterministic Turing machine</a>, then all problems in NP could be solved in polynomial time, and so the <a href="Complexity_class" title="Complexity class">complexity class</a> NP would be equal to the complexity class P.

The significance of NP-completeness was made clear by the publication in 1972 of <a href="Richard_Karp" class="mw-redirect" title="Richard Karp">Richard Karp</a>'s landmark paper, "Reducibility among combinatorial problems", in which he showed that <a href="Karp's_21_NP-complete_problems" title="Karp's 21 NP-complete problems">21 diverse combinatorial and graph theoretical problems</a>, each infamous for its intractability, are NP-complete.<a href="#cite_note-Karp-1">[1]</a>

Karp showed each of his problems to be NP-complete by reducing another problem (already shown to be NP-complete) to that problem. For example, he showed the problem 3SAT (the <a href="Boolean_satisfiability_problem" title="Boolean satisfiability problem">Boolean satisfiability problem</a> for expressions in <a href="Conjunctive_normal_form" title="Conjunctive normal form">conjunctive normal form</a> (CNF) with exactly three variables or negations of variables per clause) to be NP-complete by showing how to reduce (in polynomial time) any instance of SAT to an equivalent instance of 3SAT.<a href="#cite_note-15">[15]</a>

Garey and Johnson presented more than 300 NP-complete problems in their book Computers and Intractability: A Guide to the Theory of NP-Completeness,<a href="#cite_note-16">[16]</a> and new problems are still being discovered to be within that complexity class.

Although many practical instances of SAT can be <a href="Boolean_satisfiability_problem#Algorithms_for_solving_SAT" title="Boolean satisfiability problem">solved by heuristic methods</a>, the question of whether there is a deterministic polynomial-time algorithm for SAT (and consequently all other NP-complete problems) is still a famous unsolved problem, despite decades of intense effort by complexity theorists, <a href="Mathematical_logician" class="mw-redirect" title="Mathematical logician">mathematical logicians</a>, and others. For more details, see the article <a href="P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a>.

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFKarp1972" class="citation book cs1"><a href="Richard_Karp" class="mw-redirect" title="Richard Karp">Karp, Richard M.</a> (1972). "Reducibility Among Combinatorial Problems". In Raymond E. Miller; James W. Thatcher (eds.). Complexity of Computer Computations. New York: Plenum. pp. 85–103. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-306-30707-3</bdi>.</cite>

</li>

<li id="cite_note-2"><a href="#cite_ref-2">^</a> <cite id="CITEREFCook1971" class="citation book cs1"><a href="Stephen_Cook" title="Stephen Cook">Cook, Stephen</a> (1971). <a rel="nofollow" class="external text" href="http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=805047">"The complexity of theorem proving procedures"</a>. Proceedings of the Third Annual ACM Symposium on Theory of Computing. pp. 151–158. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F800157.805047">10.1145/800157.805047</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9781450374644</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:7573663">7573663</a>.</cite>

</li>

<li id="cite_note-3"><a href="#cite_ref-3">^</a> <cite id="CITEREFT._P._BakerJ._GillR._Solovay1975" class="citation journal cs1">T. P. Baker; J. Gill; R. Solovay (1975). "Relativizations of the P = NP question". SIAM Journal on Computing. 4 (4): 431–442. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1137%2F0204037">10.1137/0204037</a>.</cite>

</li>

<li id="cite_note-4"><a href="#cite_ref-4">^</a> <cite id="CITEREFDekhtiar1969" class="citation journal cs1 cs1-prop-foreign-lang-source">Dekhtiar, M. (1969). "On the impossibility of eliminating exhaustive search in computing a function relative to its graph". <a href="Proceedings_of_the_USSR_Academy_of_Sciences" title="Proceedings of the USSR Academy of Sciences">Proceedings of the USSR Academy of Sciences</a> (in Russian). 14: 1146–1148.</cite>

</li>

<li id="cite_note-5"><a href="#cite_ref-5">^</a> <cite id="CITEREFLevin1973" class="citation journal cs1 cs1-prop-foreign-lang-source"><a href="Leonid_Levin" title="Leonid Levin">Levin, Leonid</a> (1973). <a rel="nofollow" class="external text" href="https://www.mathnet.ru/eng/ppi914">"Универсальные задачи перебора"</a> [Universal search problems]. Problems of Information Transmission (in Russian). 9 (3): 115–116.</cite> Translated into English by <cite id="CITEREFTrakhtenbrot1984" class="citation journal cs1"><a href="Boris_Trakhtenbrot" title="Boris Trakhtenbrot">Trakhtenbrot, B. A.</a> (1984). "A survey of Russian approaches to perebor (brute-force searches) algorithms". <a href="Annals_of_the_History_of_Computing" class="mw-redirect" title="Annals of the History of Computing">Annals of the History of Computing</a>. 6 (4): 384–400. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FMAHC.1984.10036">10.1109/MAHC.1984.10036</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:950581">950581</a>.</cite> Translation see appendix, p.399-400.

</li>

<li id="cite_note-6"><a href="#cite_ref-6">^</a> This column uses the <a href="Big_O_notation" title="Big O notation">big O notation</a>.

</li>

<li id="cite_note-7"><a href="#cite_ref-7">^</a> The number of literals in each clause does not depend on <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy">, except for the last table row, which leads to a clause with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(p(n))}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(p(n))}</annotation>

</semantics>

</math><img src="./a6282d62acd69fcf285bd848594f4daafd2b4a3e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.956ex; height:2.843ex;" alt="{\displaystyle O(p(n))}" loading="lazy"> literals.

</li>

<li id="cite_note-8"><a href="#cite_ref-8">^</a> <cite id="CITEREFClaus-Peter_Schnorr1978" class="citation journal cs1">Claus-Peter Schnorr (Jan 1978). <a rel="nofollow" class="external text" href="https://www.ccs.neu.edu/home/viola/classes/papers/Schnorr-SatNQL.pdf">"Satisfiability is quasilinear complete in NQL"</a> (PDF). Journal of the ACM. 25 (1): 136–145. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F322047.322060">10.1145/322047.322060</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:1929802">1929802</a>.</cite>

</li>

<li id="cite_note-9"><a href="#cite_ref-9">^</a> <cite id="CITEREFNicholas_Pippenger_and_Michael_J._Fischer1979" class="citation journal cs1">Nicholas Pippenger and Michael J. Fischer (Apr 1979). <a rel="nofollow" class="external text" href="https://www.ccs.neu.edu/home/viola/classes/papers/PippengerF-Oblivious.pdf">"Relations among complexity measures"</a> (PDF). Journal of the ACM. 26 (2): 361–381. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F322123.322138">10.1145/322123.322138</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:2432526">2432526</a>.</cite>

</li>

<li id="cite_note-10"><a href="#cite_ref-10">^</a> <cite id="CITEREFJohn_Michael_Robson1979" class="citation conference cs1">John Michael Robson (Feb 1979). A new proof of the NP completeness of satisfiability. Proceedings of the 2nd Australian Computer Science Conference. pp. 62–70.</cite>

</li>

<li id="cite_note-11"><a href="#cite_ref-11">^</a> <cite id="CITEREFJohn_Michael_Robson1991" class="citation journal cs1">John Michael Robson (May 1991). <a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0304-3975%2891%2990177-4">"An <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(T\log T)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(T\log T)}</annotation>

</semantics>

</math><img src="./4a4f210f3928c0cb3b8d993a995ccc474cbd6bbf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.601ex; height:2.843ex;" alt="{\displaystyle O(T\log T)}" loading="lazy"> reduction from RAM computations to satisfiability"</a>. Theoretical Computer Science. 82 (1): 141–149. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0304-3975%2891%2990177-4">10.1016/0304-3975(91)90177-4</a>.</cite>

</li>

<li id="cite_note-12"><a href="#cite_ref-12">^</a> <cite id="CITEREFStephen_A._Cook1988" class="citation journal cs1">Stephen A. Cook (Jan 1988). <a rel="nofollow" class="external text" href="https://www.ccs.neu.edu/home/viola/classes/papers/Cook1988.pdf">"Short propositional formulas represent nondeterministic computations"</a> (PDF). Information Processing Letters. 26 (5): 269–270. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0020-0190%2888%2990152-4">10.1016/0020-0190(88)90152-4</a>.</cite>

</li>

<li id="cite_note-13"><a href="#cite_ref-13">^</a> <cite id="CITEREFGary_L._PetersonJohn_H._Reif1979" class="citation conference cs1">Gary L. Peterson; John H. Reif (1979). <a rel="nofollow" class="external text" href="https://ieeexplore.ieee.org/document/4568030">"Multiple-person alternation"</a>. In Ronald V. Book; Paul Young (eds.). Proc. 20th Annual <a href="Symposium_on_Foundations_of_Computer_Science" title="Symposium on Foundations of Computer Science">Symposium on Foundations of Computer Science</a> (SFCS). IEEE. pp. 348–363.</cite>

</li>

<li id="cite_note-14"><a href="#cite_ref-14">^</a> <cite id="CITEREFGary_PetersonJohn_ReifSalman_Azhar2001" class="citation journal cs1">Gary Peterson; John Reif; Salman Azhar (Apr 2001). <a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS0898-1221%2800%2900333-3">"Lower bounds for multiplayer noncooperative games of incomplete information"</a>. Computers & Mathematics with Applications. 41 (7–8): 957–992. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS0898-1221%2800%2900333-3">10.1016/S0898-1221(00)00333-3</a>.</cite>

</li>

<li id="cite_note-15"><a href="#cite_ref-15">^</a> First modify the proof of the Cook–Levin theorem, so that the resulting formula is in conjunctive normal form, then introduce new variables to split clauses with more than 3 atoms. For example, the clause <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\lor B\lor C\lor D)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (A\lor B\lor C\lor D)}</annotation>

</semantics>

</math><img src="./337ab63baa824843d0aafcffbebab183d8dea4be.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.755ex; height:2.843ex;" alt="{\displaystyle (A\lor B\lor C\lor D)}" loading="lazy"> can be replaced by the conjunction of clauses <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\lor B\lor Z)\land (\lnot Z\lor C\lor D)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (A\lor B\lor Z)\land (\lnot Z\lor C\lor D)}</annotation>

</semantics>

</math><img src="./5091cbf2695dbce6451e13f4fb2ae8a7bc1fc938.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:28.64ex; height:2.843ex;" alt="{\displaystyle (A\lor B\lor Z)\land (\lnot Z\lor C\lor D)}" loading="lazy">, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Z}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Z}</annotation>

</semantics>

</math><img src="./1cc6b75e09a8aa3f04d8584b11db534f88fb56bd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.68ex; height:2.176ex;" alt="{\displaystyle Z}" loading="lazy"> is a new variable that will not be used anywhere else in the expression. Clauses with fewer than three atoms can be padded; for example, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\lor B)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (A\lor B)}</annotation>

</semantics>

</math><img src="./39ccf97709eacad945b83238a85ec89cc220fed5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.899ex; height:2.843ex;" alt="{\displaystyle (A\lor B)}" loading="lazy"> can be replaced by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\lor B\lor B)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (A\lor B\lor B)}</annotation>

</semantics>

</math><img src="./aa5d1100c7b08f983944cc604a68e1410d8ce8b0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.246ex; height:2.843ex;" alt="{\displaystyle (A\lor B\lor B)}" loading="lazy">.

</li>

<li id="cite_note-16"><a href="#cite_ref-16">^</a> <cite id="CITEREFGareyJohnson1979" class="citation book cs1"><a href="Michael_Garey" title="Michael Garey">Garey, Michael R.</a>; <a href="David_S._Johnson" title="David S. Johnson">Johnson, David S.</a> (1979). <a href="Computers_and_Intractability" title="Computers and Intractability">Computers and Intractability: A Guide to the Theory of NP-Completeness</a>. Series of Books in the Mathematical Sciences (1st ed.). New York: <a href="W._H._Freeman_and_Company" title="W. H. Freeman and Company">W. H. Freeman and Company</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780716710455</bdi>. <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=0519066">0519066</a>. <a href="OCLC_(identifier)" class="mw-redirect" title="OCLC (identifier)">OCLC</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/oclc/247570676">247570676</a>.</cite>

</li>

</ol></div></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-05-13" href="https://en.wikipedia.org/wiki/?title=Cook%E2%80%93Levin_theorem&oldid=1290159500">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>